\begin{tabbing}
AtomFreeDecls($X$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$i$, $x$:Id. AtomFree(Type;1of(2of(2of(2of(2of(2of($X$))))))($i$,$x$)))\+
\\[0ex]\& (\=$\forall$$i$:Id, $k$:Knd.\+
\\[0ex]AtomFree(Type;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of($X$))))))))))($k$,$i$)))
\-\-
\end{tabbing}